Unbounded model checking of invariant properties is typically solved using symbolic reachability. However, BDD-based reachability methods tend to suffer from inconsistency in performance, making it difficult to identify a particular method for a given problem.